p:( List), F, G:({0..||p||}).
(q:. (q  p)  0  q)
 (x:{0..||p||}. F(x)  G(x))
 weighted-sum(p;F)  weighted-sum(p;G) 

latex

Definitions

x:A. B(x), Void, t  T, x:A.B(x), Top, x:AB(x), type List, , S  T, P  Q, #$n, {i..j}, Type, , r  s, (x  l), , f(a), , A  B, {x:A| B(x)} , i  j , a < b, False, A, -n, n+m, n - m, ||as||, True, ws_nil{ws_nil_compseq_tag_def:ObjectId}(F), ws_single{ws_single_compseq_tag_def:ObjectId}(F; p), P  Q, T, x:A  B(x), P & Q, P  Q, [], [car / cdr], as @ bs, s ~ t, i  j < k, , A  B, , s = t, EquivRel(T;x,y.E(x;y)), tt, qeq(r;s), x,y. t(x;y), x,y:A//B(x;y), a  b, {T}, P  Q, x.A(x), weighted-sum(p;F), <a, b>, SQType(T), r * s, left + right, Dec(P), r < s, a < b, r + s

Lemmas

qle transitivity qorder, qadd com, grp op preserves le qorder, mon assoc q, mon ident q, weighted-sum wf, qadd wf, qmul zero qrng, qless complement qorder, qle antisymmetry, qmul preserves qle, int-rational, decidable qless, qmul comm qrng, qmul wf, cons member, quotient wf, b-union wf, int nzero wf, bool wf, qeq wf2, btrue wf, squash wf, true wf, weighted-sum-split, le wf, non neg length, ge wf, nat properties, nat wf, rationals wf, l member wf, qle wf, int inc rationals, int seg wf, length wf1, length wf nat, top wf